Search Results

Documents authored by Krivine, Jean

Found 2 Possible Name Variants:

Krivine, Jean

Document
Short Paper
DOI: 10.4230/OASIcs.Tokenomics.2020.10
Revisiting the Liquidity/Risk Trade-Off with Smart Contracts (Short Paper)

Authors: Vincent Danos, Jean Krivine, and Julien Prat

Published in: OASIcs, Volume 82, 2nd International Conference on Blockchain Economics, Security and Protocols (Tokenomics 2020)

Abstract
Real-time financial settlements constrain traders to have the cash on hand before they can enter a trade [Khapko and Zoican, 2017]. This prevents short-selling and ultimately impedes liquidity. We propose a novel trading protocol which relaxes the cash constraint, and manages chains of deferred payments. Traders can buy without paying first, and can re-sell while still withholding payments. Trades naturally arrange in chains which contract when deals are closed and extend when new ones open. Default risk is handled by reversing trades. In this short note we propose a class of novel financial instruments for zero-risk and zero-collateral intermediation. The central idea is that bilateral trades can be chained into trade lines. The ownership of an underlying asset becomes distributed among traders with positions in the trade line. The trading protocol determines who ends up owning that asset and the overall payoffs of the participants. Counterparty risk is avoided because the asset itself serves as a collateral for the entire chain of trades. The protocol can be readily implemented as a smart contract on a blockchain. Additional examples, proofs, protocol variants, and game-theoretic properties related to the order-sensitivity of the games defined by trade lines can be found in the extended version of this note [Danos et al., 2019]. Therein, one can also find the definition and game-theoretic analysis of standard trade-lines with applications to trust-less zero-collateral intermediation.
Cite as

Vincent Danos, Jean Krivine, and Julien Prat. Revisiting the Liquidity/Risk Trade-Off with Smart Contracts (Short Paper). In 2nd International Conference on Blockchain Economics, Security and Protocols (Tokenomics 2020). Open Access Series in Informatics (OASIcs), Volume 82, pp. 10:1-10:5, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{danos_et_al:OASIcs.Tokenomics.2020.10,
  author =	{Danos, Vincent and Krivine, Jean and Prat, Julien},
  title =	{{Revisiting the Liquidity/Risk Trade-Off with Smart Contracts}},
  booktitle =	{2nd International Conference on Blockchain Economics, Security and Protocols (Tokenomics 2020)},
  pages =	{10:1--10:5},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-157-3},
  ISSN =	{2190-6807},
  year =	{2021},
  volume =	{82},
  editor =	{Anceaume, Emmanuelle and Bisi\`{e}re, Christophe and Bouvard, Matthieu and Bramas, Quentin and Casamatta, Catherine},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/OASIcs.Tokenomics.2020.10},
  URN =		{urn:nbn:de:0030-drops-135325},
  doi =		{10.4230/OASIcs.Tokenomics.2020.10},
  annote =	{Keywords: Electronic trading, Smart contracts, Static analysis}
}
Document
DOI: 10.4230/DagRep.2.8.99
Information Flow and Its Applications (Dagstuhl Seminar 12352)

Authors: Samson Abramsky, Jean Krivine, and Michael W. Mislove

Published in: Dagstuhl Reports, Volume 2, Issue 8 (2013)

Abstract
This report documents the program and the outcomes of Dagstuhl Seminar 12352 "Information Flow and Its Applications". This seminar brought together mathematicians, computer scientists, physicists and researchers from related disciplines such as computational biology who are working on problems concerning information and information flow.
Cite as

Samson Abramsky, Jean Krivine, and Michael W. Mislove. Information Flow and Its Applications (Dagstuhl Seminar 12352). In Dagstuhl Reports, Volume 2, Issue 8, pp. 99-112, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)

Copy BibTex To Clipboard

@Article{abramsky_et_al:DagRep.2.8.99,
  author =	{Abramsky, Samson and Krivine, Jean and Mislove, Michael W.},
  title =	{{Information Flow and Its Applications (Dagstuhl Seminar 12352)}},
  pages =	{99--112},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2013},
  volume =	{2},
  number =	{8},
  editor =	{Abramsky, Samson and Krivine, Jean and Mislove, Michael W.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DagRep.2.8.99},
  URN =		{urn:nbn:de:0030-drops-37866},
  doi =		{10.4230/DagRep.2.8.99},
  annote =	{Keywords: Information flow; semantics of computation; quantum computing; systems biology; information theory; informatics}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2012.276
Graphs, Rewriting and Pathway Reconstruction for Rule-Based Models

Authors: Vincent Danos, Jerome Feret, Walter Fontana, Russell Harmer, Jonathan Hayman, Jean Krivine, Chris Thompson-Walsh, and Glynn Winskel

Published in: LIPIcs, Volume 18, IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2012)

Abstract
In this paper, we introduce a novel way of constructing concise causal histories (pathways) to represent how specified structures are formed during simulation of systems represented by rule-based models. This is founded on a new, clean, graph-based semantics introduced in the first part of this paper for Kappa, a rule-based modelling language that has emerged as a natural description of protein-protein interactions in molecular biology [Bachman 2011]. The semantics is capable of capturing the whole of Kappa, including subtle side-effects on deletion of structure, and its structured presentation provides the basis for the translation of techniques to other models. In particular, we give a notion of trajectory compression, which restricts a trace culminating in the production of a given structure to the actions necessary for the structure to occur. This is central to the reconstruction of biochemical pathways due to the failure of traditional techniques to provide adequately concise causal histories, and we expect it to be applicable in a range of other modelling situations.
Cite as

Vincent Danos, Jerome Feret, Walter Fontana, Russell Harmer, Jonathan Hayman, Jean Krivine, Chris Thompson-Walsh, and Glynn Winskel. Graphs, Rewriting and Pathway Reconstruction for Rule-Based Models. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2012). Leibniz International Proceedings in Informatics (LIPIcs), Volume 18, pp. 276-288, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)

Copy BibTex To Clipboard

@InProceedings{danos_et_al:LIPIcs.FSTTCS.2012.276,
  author =	{Danos, Vincent and Feret, Jerome and Fontana, Walter and Harmer, Russell and Hayman, Jonathan and Krivine, Jean and Thompson-Walsh, Chris and Winskel, Glynn},
  title =	{{Graphs, Rewriting and Pathway Reconstruction for Rule-Based Models}},
  booktitle =	{IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2012)},
  pages =	{276--288},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-47-7},
  ISSN =	{1868-8969},
  year =	{2012},
  volume =	{18},
  editor =	{D'Souza, Deepak and Radhakrishnan, Jaikumar and Telikepalli, Kavitha},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2012.276},
  URN =		{urn:nbn:de:0030-drops-38669},
  doi =		{10.4230/LIPIcs.FSTTCS.2012.276},
  annote =	{Keywords: concurrency, rule-based models, graph rewriting, pathways, causality}
}

Krivine, Jean-Louis

Document
DOI: 10.4230/LIPIcs.CSL.2016.25
Bar Recursion in Classical Realisability: Dependent Choice and Continuum Hypothesis

Authors: Jean-Louis Krivine

Published in: LIPIcs, Volume 62, 25th EACSL Annual Conference on Computer Science Logic (CSL 2016)

Abstract
This paper is about the bar recursion operator in the context of classical realizability. The pioneering work of Berardi, Bezem, Coquand was enhanced by Berger and Oliva. Then Streicher has shown, by means of their bar recursion operator, that the realizability models of ZF, obtained from usual models of lambda-calculus (Scott domains, coherent spaces, ...), satisfy the axiom of dependent choice. We give a proof of this result, using the tools of classical realizability. Moreover, we show that these realizability models satisfy the well ordering of R and the continuum hypothesis. These formulas are therefore realized by closed lambda_c-terms. This new result allows to obtain programs from proofs of arithmetical formulas using all these axioms.
Cite as

Jean-Louis Krivine. Bar Recursion in Classical Realisability: Dependent Choice and Continuum Hypothesis. In 25th EACSL Annual Conference on Computer Science Logic (CSL 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 62, pp. 25:1-25:11, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{krivine:LIPIcs.CSL.2016.25,
  author =	{Krivine, Jean-Louis},
  title =	{{Bar Recursion in Classical Realisability: Dependent Choice and Continuum Hypothesis}},
  booktitle =	{25th EACSL Annual Conference on Computer Science Logic (CSL 2016)},
  pages =	{25:1--25:11},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-022-4},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{62},
  editor =	{Talbot, Jean-Marc and Regnier, Laurent},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2016.25},
  URN =		{urn:nbn:de:0030-drops-65650},
  doi =		{10.4230/LIPIcs.CSL.2016.25},
  annote =	{Keywords: lambda-calculus, Curry-Howard correspondence, set theory}
}
Document
DOI: 10.4230/LIPIcs.TYPES.2014.146
On the Structure of Classical Realizability Models of ZF

Authors: Jean-Louis Krivine

Published in: LIPIcs, Volume 39, 20th International Conference on Types for Proofs and Programs (TYPES 2014)

Abstract
The technique of classical realizability is an extension of the method of forcing; it permits to extend the Curry-Howard correspondence between proofs and programs, to Zermelo-Fraenkel set theory and to build new models of ZF, called realizability models. The structure of these models is, in general, much more complicated than that of the particular case of forcing models. We show here that the class of constructible sets of any realizability model is an elementary extension of the constructibles of the ground model (a trivial fact in the case of forcing, since these classes are identical). By Shoenfield absoluteness theorem, it follows that every true Sigma^1_3 formula is realized by a closed lambda_c-term.
Cite as

Jean-Louis Krivine. On the Structure of Classical Realizability Models of ZF. In 20th International Conference on Types for Proofs and Programs (TYPES 2014). Leibniz International Proceedings in Informatics (LIPIcs), Volume 39, pp. 146-161, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{krivine:LIPIcs.TYPES.2014.146,
  author =	{Krivine, Jean-Louis},
  title =	{{On the Structure of Classical Realizability Models of ZF}},
  booktitle =	{20th International Conference on Types for Proofs and Programs (TYPES 2014)},
  pages =	{146--161},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-88-0},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{39},
  editor =	{Herbelin, Hugo and Letouzey, Pierre and Sozeau, Matthieu},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2014.146},
  URN =		{urn:nbn:de:0030-drops-54953},
  doi =		{10.4230/LIPIcs.TYPES.2014.146},
  annote =	{Keywords: lambda-calculus, Curry-Howard correspondence, set theory}
}
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact